\begin{tipo}{TelCO}
	\observador{usuarios}{t: TelCO}{[Usuario]}
	\observador{gateways}{t: TelCO}{[Gateway]}
	\observador{mensajes}{t: TelCO, u: Usuario}{[(SMS, SMS)]}
		\requiere{u \in usuarios(t)}
		
	\medskip
	\invariante[usuariosDistintos]{sinRepetidos(usuarios(t))}
	\invariante[numerosDeGatewaysDistintos]{sinRepetidos([numero(g) | g \selec gateways(t)]))}
	\invariante[smsEnviadosValidos]{ (\forall u \selec usuario(t))(\forall m \selec
		mensajes (t,u))\\(\exists g \selec gateways(t)) nroDestino(prm(m)) ==
		numero(g) }
	\invariante[smsRecibidosValidos]{(\forall u \selec usuarios(t))(\forall m \selec mensajes(t, u)) nroDestino(sgd(m)) == u}
	
\end{tipo}
